the_es:event_system{i:l}, e:es-E(the_es).
((es-first(the_es; e)))  (loc(es-pred(the_es; e)) = loc(e)  Id) 

latex

Definitions	x:A. B(x), P  Q, s = t, Id, A, x:AB(x), t  T, event_system{i:l}, es-E(es), es-first(es; e), es-pred(es; e), loc(e), es-pred?(es), es_info(es), b, EOrderAxioms(E;pred?;info), P  Q, A c B, x:A  B(x)
Lemmas	event system wf